package CTL;

import java.io.File;
import java.io.PrintStream;

import rdp.RdP;
import systeme.AlgoGrapheRdP;
import systeme.GrapheRdP;



public class Main {

    public static String affiche(boolean[] b) {
	StringBuffer res = new StringBuffer();
	res.append("{ ");
	for (int i=0; i<b.length;i++) {
	    if (b[i])
		res.append(i+" ");
	}
	res.append("}");
	return res.toString();
    }

    public static void main(String[] args) {
    	String fichier = "exemples/Chameaux3.net";

		if (args.length == 1)
		
			fichier = args[0];

		// Converti le fichier en réseau de pétri 
		RdP rdp;
		try {
			rdp = new RdP(fichier);
		
			
			AlgoGrapheRdP algo = new AlgoGrapheRdP(rdp);
			
			
			GrapheRdP graphe = algo.grapheRdP();
			
			System.out.println("nbEtat =" + graphe.nbEtat + "; Franchissable="
					+ graphe.nbTransition);

		CTLAvant ctl = new CTLAvant(graphe);

		// calcul de p
		boolean[] p = ctl.prop(0);
		System.out.println("p = " + affiche(p));

		// calcul de EX(p)
		boolean[] a1 = ctl.EX(ctl.prop(0));
		System.out.println("EX(p) = " + affiche(a1));

		// calcul de AX(p)
		boolean[] a2 = ctl.AX(ctl.prop(0));
		System.out.println("AX(p)= " + affiche(a2));

		// calcul de AX(EX(p))
		boolean[] a3 = ctl.AX(a1);
		System.out.println("AX(EX(p))= " + affiche(a3));

		// calcul de EX(AX(p))
		boolean[] a4 = ctl.EX(a2);
		System.out.println("EX(AX(p))= " + affiche(a4));


		// calcul de EF(p)
		boolean[] b1 = ctl.EU(ctl.vrai(),ctl.prop(0));
		System.out.println("EF(p) = " + affiche(b1));

		// calcul de AF(p)
		boolean[] b2 = ctl.AU(ctl.vrai(),ctl.prop(0));
		System.out.println("AF(p) = " + affiche(b2));

		// calcul de EG(p) = !AF(!p)
		boolean[] b3 = ctl.neg(ctl.AU(ctl.vrai(),ctl.neg(ctl.prop(0))));
		System.out.println("EG(p) = " + affiche(b3));

		// calcul de AG(p) = !EF(!p)
		boolean[] b4 = ctl.neg(ctl.EU(ctl.vrai(),ctl.neg(ctl.prop(0))));
		System.out.println("AG(p) = " + affiche(b4));
		ecrire("toto.dot", graphe.toDot());

		} catch (Exception e) {
			e.printStackTrace();
		}
		
	
    }
    
	public static void ecrire(String fichier, String texte) {
		try {
			PrintStream f = new PrintStream(new File(fichier));
			f.print(texte);
			f.close();
		} catch (Exception e) {
			System.err.println("Probleme d'ecriture !");
		}
	}
}